/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.bool;

import java.io.BufferedReader;
import java.io.File;
import java.io.FileReader;
import java.io.IOException;
import java.io.StreamTokenizer;
import java.util.ArrayList;
import java.util.Iterator;

import alloy.api.AlloyRunner;
import alloy.util.SetOfLong;

/**
 * Represents a stencil which is a collection of {@linkplain BoolTemplateInstance instantiation}s of
 * Boolean {@linkplain BoolTemplateInstance#templCacheId template}s.
 * Can {@linkplain #allows take} a {@link BooleanFormula} {@linkplain BooleanFormula#recordCachingInfo annotated} with
 * Boolean template {@link BoolTemplateInstance information}, and
 * say whether any of the current instantiations of the template is in the stencil.
 * <p>
 * The unsatisfiable core is returned by {@link alloy.api.AlloyRunner#computeUnsatCore} in the form
 * of {@link BoolStencil}.  {@link alloy.gui.SimpleSwingASTVisitor} then uses the stencil and the
 * {@link alloy.transl.Transl}ation of a given {@link alloy.ast.Node} to determine whether a particular
 * ground instantiation of that node is in the unsatisfiable core.
 */
public class BoolStencil {
    /**
     * ArrayList where the i'th element stores the instantiations of template i that are
     * in the stencil, as a set of longs.
     */
    private ArrayList /* of SetOfLong */ _instantiationsInStencil;

    /**
     * Construct the stencil by reading it from a file.
     * The file is written by the SatLab program getAstStencil (alloy2/SatLab/src/getAstStencil).
     * That program looks at the unsatisfiable core of the CNF translation of
     * an Alloy formula (more specifically -- at the set of literals mentioned in the core),
     * and at the "instantiation file" (.ist) written by the SatLab program sat2cnf,
     */
    public BoolStencil(File stencilFileHandle_) {
		//System.out.println("reading stencil from file " + stencilFileName_);
		_instantiationsInStencil = _readStencil(stencilFileHandle_);
		//System.out.println("read stencil from " + stencilFileName_);
	}

    /**
	 * Look at a ground Boolean formula node (given by a lifted Boolean node and
	 * the current settings of {@link BoolSwitch}es on which the lifted node's
	 * {@linkplain VarConst switchable constants}depend), look which Boolean
	 * templates it {@linkplain BooleanFormula#recordCachingInfo instantiates},
	 * and test whether any of these instantiations are in the stencil. If the
	 * Boolean node has no template annotations, then just say we allow it.
	 * <p>
	 * In other words: if the ground Boolean formula does not instantiate any
	 * templates, then it is allowed by the stencil. If it does instantiate at
	 * least one template, then for each template we
	 * {@linkplain BoolTemplateInstance#compute compute}which instantiation of
	 * the Boolean template we have been passed, and check whether that
	 * instantiation of that template is in the stencil.
	 * <p>
	 * 
	 * @param bf_ a lifted Boolean DAG node; it is interpreted as a a ground
	 *            node by taking into account the current {@link BoolSwitch}
	 *            settings to interpret
	 *            {@linkplain VarConst switchable constants}as Boolean
	 *            constants.
	 * @return whether or not the given formula is allowed by the stencil,
	 *         meaning whether ornot the formula instantiates any templates
	 */
    public boolean allows(BooleanFormula bf_) {
	if (bf_.isConstantValued())
	    return true;
	
		if (bf_.getBoolTemplInsts().isEmpty())
			return true;

		for (Iterator boolTemplInstIter = bf_.getBoolTemplInsts().iterator(); boolTemplInstIter.hasNext();) {
			BoolTemplateInstance boolTemplInst = (BoolTemplateInstance) boolTemplInstIter.next();
			int boolTemplateId = boolTemplInst.getBoolTemplateId();
			if (boolTemplateId < _instantiationsInStencil.size()) {
				SetOfLong allowedInstantiations = (SetOfLong) _instantiationsInStencil.get(boolTemplateId);
				if (allowedInstantiations != null) {
					// given the current values of BoolSwitch'es,
					// which instantiation of the Boolean template
					// boolTemplateId
					// is the current ground form of bf_?
					long currentInstantiation = boolTemplInst.computeTemplKey();
					if (allowedInstantiations.contains(currentInstantiation))
						return true;
				}
			}
		}

    return false;
    }//allows

    /**
	 * Test whether a given <em>lifted</em> Boolean formula is part of the
	 * unsatisfiable core. It is if any of its ground instantiations are part of
	 * the core.
	 * 
	 * Only called from {@link AlloyRunner}.
	 * 
	 * @param bf_ a lifted Boolean DAG node; it is interpreted as a ground
	 *            node by taking into account the current {@link BoolSwitch}
	 *            settings to interpret
	 * 			 {@linkplain VarConst switchable constants} as Boolean
	 *            constants.
	 * @return if the given lifted formula is part of the unsat core
	 */
    public boolean allowsLifted(BooleanFormula bf_) {
		if (bf_.getBoolTemplInsts().isEmpty())
			return true;

		if (bf_.isConstantValued())
		    return true;

		for (Iterator boolTemplInstIter = bf_.getBoolTemplInsts().iterator(); boolTemplInstIter.hasNext();) {
			BoolTemplateInstance boolTemplInst = (BoolTemplateInstance) boolTemplInstIter.next();
			int boolTemplateId = boolTemplInst.getBoolTemplateId();
			if (boolTemplateId < _instantiationsInStencil.size()) {
				SetOfLong allowedInstantiations = (SetOfLong) _instantiationsInStencil.get(boolTemplateId);
				if (allowedInstantiations != null && !allowedInstantiations.isEmpty())
					return true;
			}
		}

		return false;
	}

    /**
     * @param bf_ the {@link booleanFormula} in question
     * @return a {@link SetOfLong} of templateIds that correspond to the given {@link BooleanFormula},
     *         according to _instantiationsInStencil
     */
    public SetOfLong BfTemplates(final BooleanFormula bf_) {
    		SetOfLong templates = new SetOfLong();
		if (bf_.getBoolTemplInsts().isEmpty())
			return templates;

		for (Iterator boolTemplInstIter = bf_.getBoolTemplInsts().iterator(); boolTemplInstIter.hasNext();) {
			BoolTemplateInstance boolTemplInst = (BoolTemplateInstance) boolTemplInstIter.next();
			int boolTemplateId = boolTemplInst.getBoolTemplateId();
			if (boolTemplateId < _instantiationsInStencil.size()) {
				//accumulator
				templates.addAll((SetOfLong) _instantiationsInStencil.get(boolTemplateId));
			}
		}

		return templates;
	}//TODO not sure this is right

	/* ilya describes allowsLifted to rseater:

	the boolean formula bf_ is the "extended" Boolean DAG
	structure where Boolean nodes can be (besides
	constants/literals/NOT/AND/OR) switchable constants
	and switch setters.  "lifted" is another name for this
	structure (as in, lifted as opposed to ground-out).
	each assignment of switches on which the switchable
	constants below a BooleanFormula node depend turns the
	lifted BooleanFormula into a particular ground
	BooleanFormula.

	template detection can annotate some lifted
	BooleanFormula nodes as matching a given Boolean
	template with a given argument list, where the
	argument list is a vector of constant-valued
	BooleanFormulas (with no literals at the leaves).  
	a particular assignment of switch values to the
	switches turns the BooleanFormula into a ground
	Boolean formula and also turns each argument list into
	a vector of Boolean constants.  

	the stencil written by getAstStencil computes, for
	each lifted BooleanFormula that matches a Boolean
	template, which instantiations of that template are in
	the core.  so, allowsLifted answers the question:
	given the stencil, can we exclude this lifted
	BooleanFormula from the core?  we only exclude it if
	(1) it matches at least one Boolean template, and (2)
	all concrete instantiations of that Boolean template
	are NOT in the core.  so, for each Boolean template
	which this lifted BooleanFormula instantiates (the
	list of them is in bf_.boolTemplInsts), we get the set
	of concrete instantiations of that BooleanTemplate
	that went into the core.  exactly which instantiations
	went into the core we don't care here -- we just ask
	whether at least one concrete instantiation of (the
	template matched by) this lifted BooleanFormula is in
	the core.
	*/ 

    /**
	 * Read a stencil file and return the contents of the stencil as an
	 * {@link ArrayList}of {@link SetOfLong}'s, giving for each template the
	 * instantiations that are in the core. Stencil format is: one line per
	 * template, terminated with -1 on the line; line starting with -1 signals
	 * end of file. Format of each line: first number is template id, remaining
	 * numbers are instantiations. E.g.:
	 *
	 * 139 0 1 2 3 -1
	 * 140 0 1 2 3 -1
	 * 151 28 29 30 31 -1
	 * -1
	 * 
	 * this description may be out of date -- see file-formats.txt and read about .stc files
	 */
    private static ArrayList /* of SetOfLong */_readStencil(
			File stencilFileHandle_) {
		ArrayList /* of SetOfLong */stencil = new ArrayList(1024);
		try {
			StreamTokenizer stencilTokenizer = new StreamTokenizer(
					new BufferedReader(new FileReader(stencilFileHandle_)));
			stencilTokenizer.parseNumbers();
			boolean stencilDone = false;
			do {
				boolean templateDone = false;
				SetOfLong instantiations = null;
				int numInstantiations = 0;
				int gotInstantiations = 0;
				do {
					if (stencilTokenizer.nextToken() == StreamTokenizer.TT_NUMBER) {
						long n = (long) stencilTokenizer.nval;
						if (instantiations == null) {
							int templateId = (int) n;
							if (templateId == 0)
								stencilDone = true;
							else {
								stencil.ensureCapacity(templateId + 1);
								while (stencil.size() < templateId + 1)
									stencil.add(null);
								stencil.set(templateId,
										instantiations = new SetOfLong());
							}
						} else if (numInstantiations == 0) {
							numInstantiations = (int) stencilTokenizer.nval;
						} else {
							instantiations.add(n);
							if ((++gotInstantiations) == numInstantiations)
								templateDone = true;
						}
					}
				} while (!stencilDone && !templateDone);
			} while (!stencilDone);
		} catch (IOException ioe_) {
			throw new Error("I/O error reading stencil file");
		}
		return stencil;
	}
}
